\begin{tabbing}
((\% Establish inductive hypothesis \% 
\\[0ex]A\=ssert $\forall$${\it y'}$:$S$. $r$($f$(${\it y'}$),$f$($y$)) $\Rightarrow$ $P$(${\it y'}$)) \+
\\[0ex]
\\[0ex]C\=ollapseTHEN (IfLabL \+
\\[0ex][`main`,OnHyps [12;10;9;8] Thin   \% cleanup \% 
\\[0ex];`assertion`,((
\-\-\\[0ex]R\=epD) \+
\\[0ex]CollapseTHENA ((Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 3:n
\-\\[0ex])) (first\_tok :t) inil\_term)))$\cdot$]))$\cdot$
\end{tabbing}